package bcontractor.propositional.factories;

import bcontractor.api.SentenceSet;
import bcontractor.base.PureSentenceSet;
import bcontractor.propositional.PropositionalSentence;

/**
 * Factory for propositional sentence sets.
 * 
 * @author lundberg
 * 
 */
public class PropositionalSentenceSetFactory implements SentenceSetFactory<PropositionalSentence> {

	private static final int REPLACEMENT_LIMIT = 1000000;

	private final SentenceFactory<PropositionalSentence> clauseFactory;

	private final int nVariables;

	private final int nClauses;

	/**
	 * Constructor
	 * 
	 * @param clauseFactory clauseFactory
	 */
	public PropositionalSentenceSetFactory(SentenceFactory<PropositionalSentence> clauseFactory, int nVariables, int nClauses) {
		this.clauseFactory = clauseFactory;
		this.nVariables = nVariables;
		this.nClauses = nClauses;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public SentenceSet<PropositionalSentence> create() {
		PropositionalProblemBuilder builder = new PropositionalProblemBuilder(nVariables);
		while (builder.getNClauses() < nClauses) {
			builder.add(clauseFactory.create());
		}
		int replacements = 0;
		while (builder.hasMissingAtoms()) {
			replacements++;
			if (replacements > REPLACEMENT_LIMIT) {
				throw new IllegalArgumentException(String.format("Unable to create sentence set with %s variables and %s clauses.", nVariables, nClauses));
			}
			PropositionalSentence candidate = clauseFactory.create(builder.nextMissingAtom());
			if (!builder.hasClause(candidate)) {
				builder.remove(builder.getFirstClause());
				builder.add(candidate);
			}
		}
		return new PureSentenceSet<PropositionalSentence>().with(builder.getClauses());
	}
}
